-- Modelo Alloy para el problema de las 8 baldosas, o Baldosas Deslizantes.
-- Este modelo Alloy describe el problema de las 8 baldosas, y permite
-- emplear Alloy Analyzer para encontrar una solucion al problema, i.e.
-- una secuencia de movimientos que permite ubicar las baldosas en
-- su correspondiente posicion.
-- Autor: Nazareno Aguirre
-- A#o: 2007
module baldosasDeslizantes

-- Una traza de movimientos es una cadena (en el sentido asociado a
-- relaciones de orden) de configuraciones.
-- Importamos la especificacion de ordenes totales estrictos provista
-- en util/ordering.
open util/ordering[Configuracion] as confs

-- Baldosas: Las baldosas que forman parte del juego son nueve:
-- B1 a B8 y la baldosa X, que representa un slot vacio.
abstract sig Baldosa { }
one sig B1, B2, B3, B4, B5, B6, B7, B8, X extends Baldosa { }

-- Posiciones: Las posiciones de las baldosas deslizantes son 9,
-- correspondientes a cada uno de los slots de un tablero de 
-- 3x3. La posicion final para cada baldosa Bi sera Pi.
abstract sig Posicion { }
one sig P1, P2, P3, P4, P5, P6, P7, P8, P9 extends Posicion { }

-- Configuracion: La configuracion del juego esta dada por una
-- ubicacion para cada una de las baldosas. Esto se modela con una
-- funcion biyectiva entre baldosas y posiciones.
sig Configuracion {
    asig: Baldosa one -> one Posicion
}

-- Predicado init: Describe la configuracion inicial del juego.
pred init(c: Configuracion) {

    c.asig = (X -> P1) + (B2 -> P2) + (B3 -> P3) + (B4 -> P4)  + 
                 (B5 -> P5) + (B6 -> P6) + (B7 -> P7) + (B1 -> P8)  +
                 (B8 -> P9) 


/*    c.asig = (B8 -> P1) + (B3 -> P2) + (B4 -> P3) + (B7 -> P4)  + 
                 (B1 -> P5) + (B2 -> P6) + (B5 -> P7) + (B6 -> P8)  +
                 (X -> P9) */
                        
}

-- Predicado final: Describe la configuracion final deseada para el juego,
-- i.e., con cada baldosa en su posicion respectiva.
pred final(c: Configuracion) {

    c.asig = (B1 -> P1) + (B2 -> P2) + (B3 -> P3) + (B4 -> P4)  + 
                 (B5 -> P5) + (B6 -> P6) + (B7 -> P7) + (B8 -> P8)  +
                 (X -> P9) 
                        
}

-- Predicado move: Describe, por casos, los movimientos de avance posibles
-- asociados al juego de las baldosas deslizantes.
pred move(c, c': Configuracion) {
    ((X -> P1) in c.asig => (c'.asig = c.asig ++ ((X -> P2) + (c.asig.P2 -> P1)) ||
                                        c'.asig = c.asig ++ ((X -> P4) + (c.asig.P4 -> P1))))
    &&
    ((X -> P3) in c.asig => (c'.asig = c.asig ++ ((X -> P2) + (c.asig.P2 -> P3)) ||
                                        c'.asig = c.asig ++ ((X -> P6) + (c.asig.P6 -> P3))))
    &&
    ((X -> P7) in c.asig => (c'.asig = c.asig ++ ((X -> P4) + (c.asig.P4 -> P7)) ||
                                        c'.asig = c.asig ++ ((X -> P8) + (c.asig.P8 -> P7))))
    &&
    ((X -> P9) in c.asig => (c'.asig = c.asig ++ ((X -> P6) + (c.asig.P6 -> P9)) ||
                                        c'.asig = c.asig ++ ((X -> P8) + (c.asig.P8 -> P9))))
    &&
    ((X -> P2) in c.asig => (c'.asig = c.asig ++ ((X -> P1) + (c.asig.P1 -> P2)) ||
                                        c'.asig = c.asig ++ ((X -> P3) + (c.asig.P3 -> P2)) ||
                                        c'.asig = c.asig ++ ((X -> P5) + (c.asig.P5 -> P2))))
    &&
    ((X -> P4) in c.asig => (c'.asig = c.asig ++ ((X -> P1) + (c.asig.P1 -> P4)) ||
                                        c'.asig = c.asig ++ ((X -> P7) + (c.asig.P7 -> P4)) ||
                                        c'.asig = c.asig ++ ((X -> P5) + (c.asig.P5 -> P4)))) 
    &&
    ((X -> P6) in c.asig => (c'.asig = c.asig ++ ((X -> P9) + (c.asig.P9 -> P6)) ||
                                        c'.asig = c.asig ++ ((X -> P3) + (c.asig.P3 -> P6)) ||
                                        c'.asig = c.asig ++ ((X -> P5) + (c.asig.P5 -> P6))))
    &&
    ((X -> P8) in c.asig => (c'.asig = c.asig ++ ((X -> P9) + (c.asig.P9 -> P8)) ||
                                        c'.asig = c.asig ++ ((X -> P7) + (c.asig.P7 -> P8)) ||
                                        c'.asig = c.asig ++ ((X -> P5) + (c.asig.P5 -> P8))))
    &&
    ((X -> P5) in c.asig => (c'.asig = c.asig ++ ((X -> P2) + (c.asig.P2 -> P5)) ||
                                        c'.asig = c.asig ++ ((X -> P4) + (c.asig.P4 -> P5)) ||
                                        c'.asig = c.asig ++ ((X -> P6) + (c.asig.P6 -> P5)) ||
                                        c'.asig = c.asig ++ ((X -> P8) + (c.asig.P8 -> P5))))
}

-- predicado Solve: Indica en que consiste resolver el problema. Una solucion al
-- problema es una secuencia de configuraciones que comienza en init, termina
-- en final, y tal que cada par de configuraciones consecutivas esta relacionado 
-- por "move", es decir, corresponde a un avance de los admitidos por el juego.
pred Solve {

   init[confs/first] &&
   final[confs/last] &&
   (all preState: Configuracion - confs/last |
       let postState = confs/next[preState] |
           move[preState, postState])
}

run Solve for 3 but exactly 59 Configuracion
